#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "klee_change_macros.h"
#include "klee_change_functions.h"
int lib(int x) {
	if(klee_change(0,1)){
		int counter = 0;
	    while (x < 0) {
	    	x++;
		    counter++;
	    }
	    return counter;
	}else{
		if (x < 0){
		    return -x;
    	}
		else{
            while (x >= 0) {
                x = x;
            }
    		return x;
    	}
	}
}

int client(int x){
	if (x > 0) {
		return -lib(-x);
	}else{
		return lib(x);
	}
}

int main(int argc, char *argv[]) {
  int x= argv[1][0] - '0';
  return client(x);
}
